COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00004 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂AIL Professor Edsger W. Dijkstra↓Plataanstraat 5↓NL-4565 NUENEN↓The Netherlands∞
Dear Professor Dijkstra:

	Zohar Manna showed me your comments on the Perlis, et. al. paper.
I entirely agree with you.  The APL practice of giving each construct
a meaning for all feasible combinations of data types comes home to
roost when the question of proving something about APL programs.

	Incidentally, the artificial intelligentsia are also interested
in proving correctness of computer programs - whether by hand or by
program.  Enclosed is a copy of a final exam in a LISP course which
includes two programs to be written and proved correct.  Since most of
the students did well with both problems, I am encouraged to try
harder problems next time the course is taught.

.sgn